#ifndef _CACHEFLUSH_H_
#define _CACHEFLUSH_H_
#include <stdint.h>

void flush_dcache_range(uintptr_t addr, size_t size);
void inv_dcache_range(uintptr_t addr, size_t size);
void clean_dcache_range(uintptr_t addr, size_t size);

#endif /* _CACHEFLUSH_H_ */
